\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$, $B$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$),\+
\\[0ex]$f$:(($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $g$:($\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}$), $L$:event{-}info(${\it ds}$;${\it da}$) List.
\-\\[0ex]($\forall$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ $\Rightarrow$ ecl{-}trans{-}h($A$)(0,ecl{-}trans{-}state($A$;${\it L'}$)) $\Rightarrow$ ${\it L'}$ $=$ $L$)
\\[0ex]$\Rightarrow$ \=ecl{-}trans{-}state(combine{-}ecl{-}tuples($A$;$B$;$f$;$g$);$L$)\+
\\[0ex]$=$
\\[0ex]$\langle$ecl{-}trans{-}state($A$;$L$)$,\,$ecl{-}trans{-}state($B$;nil)$\rangle$
\\[0ex]$\in$ ecl{-}trans{-}type(combine{-}ecl{-}tuples($A$;$B$;$f$;$g$))
\-
\end{tabbing}